Nuprl Lemma : l_member-trivia
11,40
postcript
pdf
T
:Type,
P
:(
T
),
d
:({
i
:
T
|
P
(
i
)} List),
x
:{
i
:
T
|
P
(
i
)} . (
x
d
)
(
x
d
)
latex
Definitions
,
a
<
b
,
s
=
t
,
x
:
A
B
(
x
)
,
A
c
B
,
x
:
A
.
B
(
x
)
,
f
(
a
)
,
{
x
:
A
|
B
(
x
)}
,
P
Q
,
x
:
A
.
B
(
x
)
,
type
List
,
Type
,
,
x
:
A
B
(
x
)
,
(
x
l
)
origin
T:Type, P:(T
), d:({i:T| P(i)} List), x:{i:T| P(i)} . (x 
d) 
(x d) T:Type, P:(T), d:({i:T| P(i)} List), x:{i:T| P(i)} . (x d) (x d) 
B(x)
B
x:A. B(x) Qx:A. B(x)B(x) l)